(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


(** ** Funtions of list *)
Require Export List.
Require Export Matrix.Mat.Matrix_Module.
Require Import Matrix.MMat.MMat_def.
Import ListNotations.

Section list_functions.

Variable A:Set.
Variable Zero:A.
Variable opp:A->A.
Variable add:A->A->A.
Variable sub:A->A->A.
Variable mul:A->A->A.
Variable f:A->A->A.
Variable m n p: nat.

Definition Mfun:=@Mf A m n f.
Definition mZero:=MO A Zero m p.
Definition Madd':= @Mf A m p add.
Definition Madd:=@Mf A m n add.
Definition Msub:=@Mf A m n sub.
Definition Mopp:=@Mm A m n opp.
Definition Mmul:=@matrix_mul A Zero add mul m n p.
(* ################################################################# *)

(** ** Reasoning About List Operation Functions *)

Fixpoint product(l1:list (@Mat A m n))(l2:list (@Mat A n p)) :=
  match l1 , l2 with
    | h1::t1,h2::t2 => Madd' (Mmul h1 h2) (product t1 t2)
    | _ ,_ => mZero
  end.

(** *** list_each_comm *)
(** List Operation Commutativity :
    f a b = f b a -> f l1 l2 = f l2 l1 *)
Lemma mlist_each_comm : forall n2 (l1 l2:list (@Mat A m n)),
  (forall (a b:@Mat A m n), Mfun a b === Mfun b a)-> 
  length l1 = n2 -> length l2 = n2 -> 
  list_Meq 
  (list_each (@Mat A m n) Mfun l1 l2)
  (list_each (@Mat A m n) Mfun l2 l1).
Proof.
  induction n2.
  induction l1.
  induction l2.
  - simpl. auto.
  - simpl. auto.
  - induction l2.
    + simpl. auto.
    + simpl. intros. inversion H0.
  - induction l1.
    + induction l2.
      { simpl. auto. }
      { simpl. auto. }
    + induction l2.
      { simpl. auto. }
      { simpl. intros. split. apply H. apply IHn2;auto. }
Qed.

(** *** mlist_each_assoc *)
(** List Operation Associativity :
    f (f a b) c = f a (f b c)) ->f (f l1 l2) l3 = f l1 (f l2 l3)). *)
Lemma mlist_each_assoc: forall n2 (l1 l2 l3:list (@Mat A m n)) ,
  (forall (a b c:@Mat A m n), Mfun (Mfun a b) c === Mfun a (Mfun b c)) ->
   length l1 = n2 -> length l2 = n2 -> length l3 = n2 -> 
  list_Meq
  (list_each (@Mat A m n) Mfun (list_each (@Mat A m n) Mfun l1 l2) l3) 
  (list_each (@Mat A m n) Mfun l1 (list_each (@Mat A m n) Mfun l2 l3)).
Proof.
  induction n2.
  induction l1.
  induction l2.
  induction l3.
  - simpl. auto.
  - simpl. auto.
  - simpl. auto.
  - intros. inversion H0.
  - induction l1. induction l2. induction l3.
    + simpl. auto.
    + simpl. auto.
    + simpl. auto.
    + induction l2. induction l3.
      { simpl. auto. }
      { simpl. auto. }
      { induction l3.
        * simpl. auto.
        * simpl. intros. rewrite H. split. reflexivity.
          apply IHn2. auto. auto. auto. auto. }
Qed.

(** *** mlist_sub_opp *)
(** List substraction commutativity : 
    a-b = -(a-b) -> l1-l2 = -(l1-l2). *)
Lemma mlist_sub_opp : forall (l1 l2:list(@Mat A m n)) , 
  (forall (a b:@Mat A m n), Msub a b === Mopp (Msub b a)) -> 
  list_Meq
  (list_each (@Mat A m n) Msub l1 l2 )
  (list_map (@Mat A m n) Mopp (list_each (@Mat A m n) Msub l2 l1)).
Proof.
  induction l1.
  induction l2.
  - simpl. auto.
  - simpl. auto.
  - induction l2.
    + simpl. auto.
    + simpl. intros. auto.
Qed.

(** *** mlist_sub_comm *) 
(** List substraction commutativity2 : 
    a-b-c = a-c-b -> l1-l2-l3 = l1-l3-l2. *)
Lemma mlist_sub_comm : forall l1 l2 l3,
  (forall a b c, Msub (Msub a b) c === Msub (Msub a c) b) -> 
  list_Meq
  (list_each (@Mat A m n) Msub (list_each (@Mat A m n) Msub l1 l2) l3)
  (list_each (@Mat A m n) Msub (list_each (@Mat A m n) Msub l1 l3) l2).
Proof.
  induction l1.
  - simpl. auto.
  - induction l2. induction l3.
    + simpl. auto.
    + simpl. auto.
    + induction l3.
      { simpl. auto. }
      { simpl. intros. split. apply H. apply IHl1. auto. }
Qed.

(** *** mlist_sub_assoc *)
(** List substraction associativity : 
    a-b-c = a-(b+c) -> l1-l2-l3 = l1-(l2+l3). *)
Lemma mlist_sub_assoc : forall l1 l2 l3 ,
  (forall a b c,Msub (Msub a b) c === Msub a (Madd b c)) -> 
  list_Meq
  (list_each (@Mat A m n) Msub (list_each (@Mat A m n) Msub l1 l2) l3) 
  (list_each (@Mat A m n) Msub l1 (list_each (@Mat A m n) Madd l2 l3)).
Proof.
  induction l1.
  - simpl. auto.
  - induction l2. induction l3.
    + simpl. auto.
    + simpl. auto.
    + induction l3.
      { simpl. auto. }
      { simpl. intros. split. apply H. apply IHl1. auto. }
Qed.

End list_functions.